\begin{tabbing}
$e$ leaks $x$ to ${\it e'}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$a$:Atom1\+
\\[0ex](loc($e$) $\parallel$ $a$
\\[0ex]\& ($\neg$state when $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$\parallel$$a$)
\\[0ex]\& $e$ receives $\parallel$ $a$
\\[0ex]\& (($\uparrow$isrcv(${\it e'}$)) c$\wedge$ (sender(${\it e'}$) = $e$ \& ($\neg$val(${\it e'}$):valtype(${\it e'}$)$\parallel$$a$))))
\-
\end{tabbing}